home *** CD-ROM | disk | FTP | other *** search
/ Celestin Apprentice 2 / Apprentice-Release2.iso / Tools / Languages / Caml Light 0.61 / Binaries / examples / kb / terms.ml < prev   
Encoding:
Text File  |  1993-09-24  |  3.1 KB  |  109 lines  |  [TEXT/ttxt]
  1. (****************** Term manipulations *****************)
  2.  
  3. #open "prelude";;
  4.  
  5. type term = Var of int
  6.           | Term of string * term list;;
  7.  
  8. let rec vars = function
  9.     Var n -> [n]
  10.   | Term(_,L) -> vars_of_list L
  11. and vars_of_list = function
  12.     [] -> []
  13.   | t::r -> union (vars t) (vars_of_list r)
  14. ;;
  15.  
  16. let substitute subst = subst_rec where rec subst_rec = function
  17.     Term(oper,sons) -> Term(oper, map subst_rec sons)
  18.   | Var(n) as t     -> try assoc n subst with Not_found -> t
  19. ;;
  20.  
  21. let change f = change_rec where rec change_rec =
  22.   fun (h::t) n -> if n=1 then f h :: t else h :: change_rec t (n-1)
  23.    |    _    _ -> failwith "change"
  24. ;;
  25.  
  26. (* Term replacement replace M u N => M[u<-N] *)
  27. let replace M u N = reprec(M,u)
  28.   where rec reprec = function
  29.     _, [] -> N
  30.   | Term(oper,sons), (n::u) ->
  31.              Term(oper, change (fun P -> reprec(P,u)) sons n)
  32.   | _ -> failwith "replace"
  33. ;;
  34.  
  35. (* matching = - : (term -> term -> subst) *)
  36. let matching term1 term2 =
  37.   let rec match_rec subst = fun
  38.       (Var v) M ->
  39.         if mem_assoc v subst then
  40.           if M = assoc v subst then subst else failwith "matching"
  41.         else
  42.           (v,M) :: subst
  43.     | (Term(op1,sons1)) (Term(op2,sons2)) ->
  44.     if op1 = op2 then it_list2 match_rec subst sons1 sons2
  45.                      else failwith "matching"
  46.     | _ _ ->
  47.         failwith "matching" in
  48.   match_rec [] term1 term2
  49. ;;
  50.  
  51. (* A naive unification algorithm *)
  52.  
  53. let compsubst subst1 subst2 = 
  54.   (map (fun (v,t) -> (v, substitute subst1 t)) subst2) @ subst1
  55. ;;
  56.  
  57. let occurs n = occur_rec where rec occur_rec = function
  58.     Var m -> m=n
  59.   | Term(_,sons) -> exists occur_rec sons
  60. ;;
  61.  
  62. let rec unify = function
  63.     (Var n1 as term1), term2 ->
  64.       if term1 = term2 then []
  65.       else if occurs n1 term2 then failwith "unify1"
  66.       else [n1,term2]
  67.   | term1, Var n2 ->
  68.       if occurs n2 term1 then failwith "unify2"
  69.       else [n2,term1]
  70.   | Term(op1,sons1), Term(op2,sons2) ->
  71.       if op1 = op2 then 
  72.     it_list2 (fun s t1 t2 -> compsubst (unify(substitute s t1,
  73.                                                   substitute s t2)) s)
  74.                  [] sons1 sons2
  75.       else failwith "unify3"
  76. ;;
  77.  
  78. (* We need to print terms with variables independently from input terms
  79.   obtained by parsing. We give arbitrary names v1,v2,... to their variables. *)
  80.  
  81. let INFIXES = ["+";"*";"-";"/"];;
  82.  
  83. let rec pretty_term = function
  84.     Var n ->
  85.       print_string "v"; print_int n
  86.   | Term (oper,sons) ->
  87.       if mem oper INFIXES then
  88.         match sons with
  89.             [s1;s2] ->
  90.               pretty_close s1; print_string oper; pretty_close s2
  91.           | _ ->
  92.               failwith "pretty_term : infix arity <> 2"
  93.       else
  94.        (print_string oper;
  95.         match sons with
  96.          []   -> ()
  97.           | t::lt -> print_string "(";
  98.                      pretty_term t;
  99.                      do_list (fun t -> print_string ","; pretty_term t) lt;
  100.                      print_string ")")
  101. and pretty_close = function
  102.     Term(oper, _) as M ->
  103.       if mem oper INFIXES then
  104.         (print_string "("; pretty_term M; print_string ")")
  105.       else pretty_term M
  106.   | M -> pretty_term M
  107. ;;
  108.  
  109.